es:ES, e, e':E. (e'  es-le-before(es;e))  e' loc e  

latex

Definitions	e loc e' , x:AB(x), P  Q, P  Q, x:A  B(x), P & Q, P  Q, ES, E, x:A. B(x), (e <loc e'), (x  l), s = t, left + right, P  Q, [], [car / cdr], before(e), es-le-before(es;e)
Lemmas	event system wf, member append, member-es-before, iff functionality wrt iff, l member wf, or functionality wrt iff, es-locl wf, es-E wf, member singleton, iff wf, rev implies wf, es-le wf